A:Type, eq:EqDecider(A), B:(AType), P:(A), f:fpf(A; x.B(x)).
fpf-vals(eq; P; f)  ((x:{a:A| (P(a))}   B(x)) List) 

latex

Definitions	Unit, b, A, guard(T), prop{i:l}, P  Q, P  Q, P  Q, P  Q, strong-subtype(A; B), (x  l), remove-repeats(eq; L), P  Q, b, x. t(x), x(s), , EqDecider(T), x:A. B(x), fpf-vals(eq; P; f), fpf(A; a.B(a)), t  T, let x = a in b(x)
Lemmas	deq wf, bool wf, fpf wf, l member wf, remove-repeats wf, strong-subtype-self, strong-subtype-set3, strong-subtype-deq-subtype, cons member, subtype rel list, assert wf, not wf, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert